PolarityProjectionLike.agda:29,10-11
i != ↑ i of type Size
when checking that the expression x has type
Contra true (mkType (D (↑ i)))
